Your Proof Fails? Testing Helps to Find the Reason

摘要

Applying deductive verification to formally prove that a program respects itsformal specification is a very complex and time-consuming task due inparticular to the lack of feedback in case of proof failures. Along with anon-compliance between the code and its specification (due to an error in atleast one of them), possible reasons of a proof failure include a missing ortoo weak specification for a called function or a loop, and lack of time orsimply incapacity of the prover to finish a particular proof. This workproposes a new methodology where test generation helps to identify the reasonof a proof failure and to exhibit a counter-example clearly illustrating theissue. We describe how to transform an annotated C program into C code suitablefor testing and illustrate the benefits of the method on comprehensiveexamples. The method has been implemented in STADY, a plugin of the softwareanalysis platform FRAMA-C. Initial experiments show that detectingnon-compliances and contract weaknesses allows to precisely diagnose most prooffailures.